(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun c () Real)
(assert (or (= (+ (* 24 x2) (* (- 12) c) (* (- 11) x2) (* 21 b)) (- 25)) (not (< (+ (* (- 42) x2) (* 19 x2) (* 37 a)) 38))))
(assert (< (+ (div (- 40) x2) (* 1 x3) (* (- 30) c) (* (- 45) x2) (* 39 x3)) (- 6)))
(assert (or (not (> (+ (* 26 a) (* (- 42) b) (* (- 40) x2) (* (- 33) a) x2 (* (- 5) c) (* 46 c) (* 13 b) (* (- 94) c) (* (- 22) c) (* (- 6) b)) (- 16))) (not (<= (+ (* 48 x3) (* 27 a) (* (- 23) x2) (* (- 35) x3)) 37)) (not (<= (+ (* 25 a) (* 16 b) (* 47 x2) (* (- 22) a)) 10))))
(assert (>= (+ (* 38 a) (* 6 b) (* (- 48) b) (div (- 27) c) (* 33 b) (* (- 14) x2) (* 40 c) (* 26 x3)) 42))
(check-sat)
(push)
(check-sat)
(pop)
(assert (or (<= (+ (* (- 32) x2) (* 30 b) (* 41 x2) (* (- 37) b)) (- 21)) (< (+ (* 9 a) (* (- 1) x2) (* 48 b) (* (- 47) a) (* 49 a) 0 (* 9 b) (* (- 30) c) (* 38 x2) (* 5 a)) 19)))
(check-sat)
(assert (or (< (+ (* 28 x3) 23 (* (- 36) x2)) 0) (< (+ (* 3) (* c)) 40)))
(check-sat)
(assert (or (not (< (+ (* (- 4) a)) (- 28))) (= (+ (* 41 b) c) 0)))
(check-sat)
(check-sat)
(check-sat)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun c () Real)
(assert (or (= (+ (* 24 x2) (* (- 12) c) (* (- 11) x2) (* 21 b)) (- 25)) (not (< (+ (* (- 42) x2) (* 19 x2) (* 37 a)) 38))))
(assert (< (+ (div (- 40) x2) (* 1 x3) (* (- 30) c) (* (- 45) x2) (* 39 x3)) (- 6)))
(assert (or (not (> (+ (* 26 a) (* (- 42) b) (* (- 40) x2) (* (- 33) a) x2 (* (- 5) c) (* 46 c) (* 13 b) (* (- 94) c) (* (- 22) c) (* (- 6) b)) (- 16))) (not (<= (+ (* 48 x3) (* 27 a) (* (- 23) x2) (* (- 35) x3)) 37)) (not (<= (+ (* 25 a) (* 16 b) (* 47 x2) (* (- 22) a)) 10))))
(assert (>= (+ (* 38 a) (* 6 b) (* (- 48) b) (div (- 27) c) (* 33 b) (* (- 14) x2) (* 40 c) (* 26 x3)) 42))
(check-sat)
(push)
(check-sat)
(pop)
(assert (or (<= (+ (* (- 32) x2) (* 30 b) (* 41 x2) (* (- 37) b)) (- 21)) (< (+ (* 9 a) (* (- 1) x2) (* 48 b) (* (- 47) a) (* 49 a) 0 (* 9 b) (* (- 30) c) (* 38 x2) (* 5 a)) 19)))
(check-sat)
(assert (or (< (+ (* 28 x3) 23 (* (- 36) x2)) 0) (< (+ (* 3) (* c)) 40)))
(check-sat)
(assert (or (not (< (+ (* (- 4) a)) (- 28))) (= (+ (* 41 b) c) 0)))
(check-sat)
(check-sat)
(check-sat)
